A:Type, eq:EqDecider(A), f,g:fpf(A; a.Type), a:A.
subtype_rel(fpf-cap(fpf-join(eq; f; g); eq; a; top); fpf-cap(f; eq; a; top)) 

latex

Definitions	x:A. B(x), t  T, x. t(x), x(s), P  Q, guard(T)
Lemmas	fpf-sub-join-left, fpf-cap-subtype functionality wrt sub, fpf-join wf, fpf wf, deq wf